Lean 语言参考手册

4.4. 归纳类型🔗

归纳类型 是在 Lean 中引入新类型的主要方式。 虽然 宇宙、函数 以及 商类型 是内置的原语类型，用户无法自行添加，但 Lean 里的其它类型要么是归纳类型，要么是基于宇宙、函数与归纳类型定义的。 归纳类型的定义依赖于它们的 类型构造子 和 构造子 ；它们的其它性质也由这些定义推导而来。 每个归纳类型有唯一的类型构造子，这个构造子可能带有 宇宙参数 和普通参数。 归纳类型可以拥有任意数量的构造子；这些构造子用于生成新的值，其类型由归纳类型的类型构造子决定。

根据归纳类型的类型构造子和构造子，Lean 会自动生成一个 递归子。 从逻辑上讲，递归子代表归纳原则或消去规则；从计算角度看，它们表示原始递归计算。 递归函数的终止性由其翻译为递归子的调用来保证，因此 Lean 的内核只需对递归子的应用做类型检查，而无需单独进行终止性分析。 除此之外，Lean 还根据递归子生成很多辅助结构无论类型是否递归，递归子总会被用到，这些结构被系统的其他部分使用。

结构体 是一种特殊的归纳类型，只包含一个构造子。 当一个结构体被声明时，Lean 会自动生成辅助工具，使得新结构体能支持更多语言特性。

本节描述用于定义归纳类型和结构体的具体语法细节、归纳类型声明会在环境中引入哪些新的常量和定义，以及在编译后归纳类型值的运行时表现。

4.4.1. 归纳类型声明🔗

syntax归纳类型声明
command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      In Lean, every concrete type other than the universes
and every type constructor other than dependent arrows
is an instance of a general family of type constructions known as inductive types.
It is remarkable that it is possible to construct a substantial edifice of mathematics
based on nothing more than the type universes, dependent arrow types, and inductive types;
everything else follows from those.
Intuitively, an inductive type is built up from a specified list of constructors.
For example, `List α` is the list of elements of type `α`, and is defined as follows:
```
inductive List (α : Type u) where
| nil
| cons (head : α) (tail : List α)
```
A list of elements of type `α` is either the empty list, `nil`,
or an element `head : α` followed by a list `tail : List α`.
See [Inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html)
for more information.
inductive `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig where
        (| `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers ident `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig)*
      (deriving ident,*)?

声明一个新的归纳类型。 declModifiers 的含义可在 声明修饰词部分 查询。

声明归纳类型后，其类型构造子、构造子和递归子会添加到环境中。 新的归纳类型扩展了 Lean 的核心逻辑——它们不是由系统中已有的数据编码或模拟出来的。 归纳类型声明还必须满足一系列 良构性要求 以确保逻辑系统的一致性。

声明的第一行，从 Lean.Parser.Command.inductive : commandinductive 到 Lean.Parser.Command.inductive : commandwhere，用于指定新的 类型构造子 的名字和类型。 如果为类型构造子提供了类型签名，则结果类型必须是 宇宙，但参数不一定要是类型。 如果没有提供签名，Lean 会尝试为结果类型推断出刚好合适的宇宙。 在某些场景下，推断可能无法找到最小宇宙甚至无法推断成功，此时需要手动注释。

构造子定义在 Lean.Parser.Command.inductive : commandwhere后边。 构造子并非必需，比如像 False 和 Empty 这样没有构造子的归纳类型是完全合理的。 每个构造子定义以竖线 ('|', Unicode 'VERTICAL BAR' (U+007c))、声明修饰词和名字。 名字是 原始标识符。 名字后接声明签名。 签名可以包含任意参数，但需满足归纳类型声明的良构性要求，返回类型必须是归纳类型的类型构造子的饱和应用。 如果未指定签名，则 Lean 会插入足够的隐式参数来推断出良构的返回类型。

新归纳类型的名字定义在当前命名空间中。 每个构造子的名字位于该归纳类型的命名空间下。

4.4.1.1. 参数与索引🔗

类型构造子可以接收两类参数：参数 和 索引 。 定义中，参数必须在整个归纳类型定义中保持一致；所有构造子中出现的类型构造子，参数必须一模一样。 索引则可以在不同构造子的类型构造子的具体应用中变化。 所有参数在类型构造子的签名中必须排在索引的前面。

在类型构造子的签名中冒号（':'）之前的内容作为整个归纳类型声明的参数， 这些参数在类型定义过程中始终如一。 通常，冒号之后为索引，可以在归纳类型定义中变化。 但如果 inductive.autoPromoteIndices 选项为 true，则本来可以作为参数的语法层面的索引会被自动提升为参数。 当一个索引的所有类型依赖全都是参数类型，且它在所有构造子的类型构造子调用中始终未实例化、未变化，那么它就可以被当作参数。

🔗option
inductive.autoPromoteIndices

默认值: true

只要有可能，就应将归纳类型中的索引提升为参数。

索引实际上定义了一个类型族。 每次索引取值确定，就从族中选出一个类型，该类型有它各自的构造子。 含索引的类型构造子即定义了一个 索引族 。

4.4.1.2. 归纳类型样例🔗

一个没有构造子的类型

Vacant 是一个空的归纳类型，等价于 Lean 的 Empty 类型：

inductive Vacant : Type where

空归纳类型并非毫无用处；它们可以用于标记不可达代码。

一个没有构造子的命题

No 是一个假命题，等价于 Lean 的 False:

inductive No : Prop where
单位类型

Solo 和 Lean 的 Unit 类型等价：

inductive Solo where | solo

这是一个类型构造子和构造子的签名都被省略的例子。Lean 会将 Solo 推断为 Type：

Solo : Type#check Solo 
Solo : Type

构造子的名字是 Solo.solo，因为构造子的名字在类型构造子的命名空间下。 由于 Solo 无需参数，Lean 自动推断 Solo.solo 的类型为：

Solo.solo : Solo#check Solo.solo 
Solo.solo : Solo
真命题

Yes 等价于 Lean 的 True 命题：

inductive Yes : Prop where | intro

不同于 One，新的归纳类型 Yes 被指定为 Prop 宇宙。

Yes : Prop#check Yes 
Yes : Prop

推断得到的 Yes.intro 的签名如下：

Yes.intro : Yes#check Yes.intro 
Yes.intro : Yes
一个带参数和索引的类型

EvenOddList α b 表示一种列表，其中 α 是元素类型，b 为 true 表示含偶数个元素：

inductive EvenOddList (α : Type u) : Bool → Type u where | nil : EvenOddList α true | cons : α → EvenOddList α isEven → EvenOddList α (not isEven)

以下例子类型合法，因为列表有两个元素：

example : EvenOddList String true := .cons "a" (.cons "b" .nil)

下面这个例子类型不合法，因为实际有三个元素：

example : EvenOddList String true := type mismatch EvenOddList.cons "a" (EvenOddList.cons "b" (EvenOddList.cons "c" EvenOddList.nil)) has type EvenOddList String !!!true : Type but is expected to have type EvenOddList String true : Type.cons "a" (.cons "b" (.cons "c" .nil)) 
type mismatch
  EvenOddList.cons "a" (EvenOddList.cons "b" (EvenOddList.cons "c" EvenOddList.nil))
has type
  EvenOddList String !!!true : Type
but is expected to have type
  EvenOddList String true : Type

在本声明中，α 是 参数， 因为它在 EvenOddList 的每次出现都保持一致；b 是 索引，因为它在不同出现中可取不同值。

参数在冒号前和冒号后

在本例中，所有参数都在 Either 签名的冒号前：

inductive Either (α : Type u) (β : Type v) : Type (max u v) where | left : α → Either α β | right : β → Either α β

在下面这个版本中，有两个名为 α 的类型，可能不完全相同：

inductive Either' (α : Type u) (β : Type v) : Type (max u v) where Mismatched inductive type parameter in Either' α β The provided argument α is not definitionally equal to the expected parameter α✝ Note: The value of parameter 'α✝' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.| left : {α : Type u} → {β : Type v} → α → Either' α β | right : β → Either' α β 
Mismatched inductive type parameter in
  Either' α β
The provided argument
  α
is not definitionally equal to the expected parameter
  α✝

Note: The value of parameter 'α✝' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.

把参数放在冒号后，则对应的构造子参数可以由构造子自行实例化：

inductive Either'' : Type u → Type v → Type (max u v + 1) where | left : {α : Type u} → {β : Type v} → α → Either'' α β | right : β → Either'' α β

此时需要更大的宇宙层级，因为 构造子的参数必须处于比归纳类型本身更低的宇宙。 Either''.right 的类型参数会按 Lean 的 自动隐式参数 规则推断。

4.4.1.3. 匿名构造子语法🔗

如果归纳类型只有一个构造子，则这个构造子可以使用 匿名构造子语法。 即，不必写出构造子的名字并将其应用到参数上，而直接把所有显式参数用尖括号（'⟨' 和 '⟩', Unicode MATHEMATICAL LEFT ANGLE BRACKET (U+0x27e8) 和 MATHEMATICAL RIGHT ANGLE BRACKET (U+0x27e9)）括起来，并用逗号分隔即可。 这种语法可以用于模式匹配和表达式。 若想按照参数名字提供参数，或将所有隐式参数变为显式，则需使用普通构造子语法。

syntax匿名构造子

可通过用尖括号括起所有显式参数并用逗号分隔，匿名地调用构造子。

term ::= ...
    | The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the
expected type is an inductive type with a single constructor `c`.
If more terms are given than `c` has parameters, the remaining arguments
are turned into a new anonymous constructor application. For example,
`⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`.
⟨ term,* ⟩
匿名构造子

类型 AtLeastOne α 和 List α 相似，区别在于它始终至少有一个元素：

inductive AtLeastOne (α : Type u) : Type u where | mk : α → Option (AtLeastOne α) → AtLeastOne α

可采用匿名构造子语法进行构造：

def oneTwoThree : AtLeastOne Nat := ⟨1, some ⟨2, some ⟨3, none⟩⟩⟩

也可用该语法进行模式匹配：

def AtLeastOne.head : AtLeastOne α → α | ⟨x, _⟩ => x

同样，传统构造子语法也可以：

def oneTwoThree' : AtLeastOne Nat := .mk 1 (some (.mk 2 (some (.mk 3 none)))) def AtLeastOne.head' : AtLeastOne α → α | .mk x _ => x

4.4.1.4. 派生实例🔗

归纳类型声明末尾可选的 Lean.Parser.Command.inductive : commandderiving 子句，可用于自动派生类型类实例。 详情请见 关于实例自动派生的章节。

4.4.2. 结构体声明🔗

结构体 是只有一个构造子、无下标的归纳类型。 作为这些约束的交换，Lean 会为结构体自动生成一些便捷功能：为每个字段生成投影函数、允许基于字段名（而非位置参数）的新构造语法、同样可以按指定字段名修改值，并且结构体可以扩展其它结构体。 结构体和其它归纳类型一样，可以递归定义；它们必须遵守严格正性限制。 结构体本身并没有带来 Lean 表达力的增强；它们的所有特性都是通过代码生成机制实现的。

4.4.2.1. 结构体参数🔗

与普通归纳类型声明相同，结构体声明的头部可以包含参数和结果宇宙层级。 结构体不能定义 索引族。

4.4.2.2. 字段🔗

结构体声明的每个字段，都对应构造子的一个参数。 每个字段中都会独立插入自动隐式参数,即使名称相同，且这些字段会成为构造子的参数以量化类型。

结构体字段中的自动隐式参数

结构体 MyStructure 包含一个字段，其类型是自动隐式参数：

structure MyStructure where field1 : α field2 : α

类型构造子 MyStructure 需要两个宇宙参数：

MyStructure.{u, v} : Type (max u v)

由于构造子字段量化于 Sort 中的类型，因此其结果类型是 Type，而非 Sort。具体来说，构造子 MyStructure.mk 的两个字段都带有隐式类型参数：

MyStructure.mk.{u, v} (field1 : {α : Sort u} → α) (field2 : {α : Sort v} → α) : MyStructure.{u,v}

对于每个字段，都会自动生成一个 投影函数，用于从构造子中提取字段的值。 这个函数在结构体名称对应的命名空间中。 结构体字段投影由繁释器特别处理（具体见 结构体继承），其行为比仅查找命名空间要复杂。 当字段类型依赖于之前字段时，依赖型投影函数的类型会使用之前的投影表达，而不是显式模式匹配。

依赖型投影类型

结构体 ArraySized 包含一个字段，其类型依赖于结构体参数和先前字段：

structure ArraySized (α : Type u) (length : Nat) where array : Array α size_eq_length : array.size = length

投影函数 size_eq_length 的签名中，会隐式带入结构体类型的参数，通过先前的投影引用之前的字段：

ArraySized.size_eq_length.{u} {α : Type u} {length : Nat} (self : ArraySized α length) : self.array.size = length

结构体字段可以通过 := 指定默认值。 如果没有提供该字段的显式值，则使用默认值。

默认值

图的邻接表可用一个 Nat 列表的数组表示。 数组大小代表顶点数，数组中每个元素（通过顶点下标访问）存储对应顶点的出边。 由于 adjacency 字段提供了默认值 #[]，空图 Graph.empty 在构造时无需提供字段值。

structure Graph where adjacency : Array (List Nat) := #[] def Graph.empty : Graph := {}

结构体字段还可以通过索引以点号访问。 字段编号从 1 开始。

4.4.2.3. 结构体构造子🔗

结构体构造子可以通过在字段前加构造子名称与 :: 显式命名。 若未显式指定名称，则构造子在结构体命名空间中名为 mk。 声明修饰符 也可被用于显式构造子名称前。

非默认构造子名称

结构体 Palindrome 包含一个字符串以及显示该字符串反转与原字相等的证明：

structure Palindrome where ofString :: text : String is_palindrome : text.data.reverse = text.data

其构造子为 Palindrome.ofString，而非 Palindrome.mk。

结构体构造子的修饰符

结构体 NatStringBimap 表示自然数与字符串之间的有限双射。 它由一对映射组成，每个映射的键在另一个映射的值中也仅出现一次。 由于构造子被声明为 private，定义模块之外的代码无法直接构造新实例，只能通过维护类型不变性的 API 构造。 同时，显式指定默认构造子名称时，可以给构造子加上 文档注释。

structure NatStringBimap where /-- 在一些自然数和字符串之间构建一个有限双射 -/ private mk :: natToString : Std.HashMap Nat String stringToNat : Std.HashMap String Nat def NatStringBimap.empty : NatStringBimap := ⟨{}, {}⟩ def NatStringBimap.insert (nat : Nat) (string : String) (map : NatStringBimap) : Option NatStringBimap := if map.natToString.contains nat || map.stringToNat.contains string then none else some (NatStringBimap.mk (map.natToString.insert nat string) (map.stringToNat.insert string nat))

由于结构体本质上就是单构造子的归纳类型，其构造子既可以直接调用或用于匿名构造子语法下的模式匹配, 也可以用 结构体实例 记法（含有实字段名和值）进行构造或模式匹配。

syntax结构体实例
term ::= ...
    | Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
inherited. If `e` is itself a variable called `x`, it can be elided:
`fun y => { x := 1, y }`.
A *structure update* of an existing value can be given via `with`:
`{ point with x := 1 }`.
The structure type can be specified if not inferable:
`{ x := 1, y := 2 : Point }`.
{ structInstField,*
        (: term)? }

指定字段名及其值来构造一个结构体类型的值。 字段说明可有两种形式：

structInstField ::= ...
    | structInstLVal := term
structInstField ::= ...
    | ident

structInstLVal 可以是字段名（标识符）、字段索引（自然数），或带中括号的项，并可接零个或多个子字段。 子字段可以是带点的字段名或索引，也可以是带中括号的项。

该语法在繁释时会转换为结构体构造子的应用。 字段以名称分配，顺序不限。 子字段赋值用于初始化嵌套在字段中的结构体的字段。 在构造结构体时不允许带中括号的项，中括号用于结构体更新。

不带 := 的字段被认为是字段缩写。 此时，标识符 f 等价于 f := f，即作用域中的 f 会被用于字段赋值。

所有无默认值的字段，都需要明确提供。 如果默认参数指定为 tactic，那么在繁释阶段会运行 tactic 求得参数值。

在模式匹配语境下，字段名映射到能匹配相应投影的模式，字段缩写可直接绑定同名模式变量。 默认参数同样适用于模式；如果模式未指定带默认值字段的值，则模式只匹配默认值。

可选类型注解允许在类型无法直接唯一确定时明确指定结构体类型。

模式与默认值

结构体 AugmentedIntList 包含一个整数列表及一些可选额外信息（默认为空字符串）：

structure AugmentedIntList where list : List Int augmentation : String := ""

在测试列表是否为空时，函数 isEmpty 还会检测字段 augmentation 是否为空；因为忽略字段会采用默认值，模式匹配同样如此：

def AugmentedIntList.isEmpty : AugmentedIntList → Bool | {list := []} => true | _ => false false#eval {list := [], augmentation := "extra" : AugmentedIntList}.isEmpty 
false
syntax结构体更新
term ::= ...
    | Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
inherited. If `e` is itself a variable called `x`, it can be elided:
`fun y => { x := 1, y }`.
A *structure update* of an existing value can be given via `with`:
`{ point with x := 1 }`.
The structure type can be specified if not inferable:
`{ x := 1, y := 2 : Point }`.
{term with
        structInstField,*
        (: term)?}

对构造子类型的值进行更新。 Lean.Parser.Term.structInst : termStructure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be inherited. If `e` is itself a variable called `x`, it can be elided: `fun y => { x := 1, y }`. A *structure update* of an existing value can be given via `with`: `{ point with x := 1 }`. The structure type can be specified if not inferable: `{ x := 1, y := 2 : Point }`. with 子句之前的项应为结构体类型值，即待更新的原值。 新的结构体实例中，所有未指定的字段都从原始值拷贝，指定字段被覆盖为新值。 更新结构体时，也可以通过中括号带索引更新数组字段。 索引表达式不要求越界，越界更新会被忽略。

数组更新

结构体更新可以用字段名，也可以用数组索引。 越界索引的更新会被直接忽略：

structure AugmentedIntArray where array : Array Int augmentation : String := "" deriving Repr def one : AugmentedIntArray := {array := #[1]} def two : AugmentedIntArray := {one with array := #[1, 2]} def two' : AugmentedIntArray := {two with array[0] := 2} def two'' : AugmentedIntArray := {two with array[99] := 3} ({ array := #[1], augmentation := "" }, { array := #[1, 2], augmentation := "" }, { array := #[2, 2], augmentation := "" }, { array := #[1, 2], augmentation := "" })#eval (one, two, two', two'') 
({ array := #[1], augmentation := "" },
 { array := #[1, 2], augmentation := "" },
 { array := #[2, 2], augmentation := "" },
 { array := #[1, 2], augmentation := "" })

结构体类型的值也可以使用 Lean.Parser.Command.declValEqns : commandwhere， 在定义后为每个字段赋值，只能用于定义体，不能在通用表达式中用。

结构体中的 where

Lean 中的乘积类型是名为 Prod 的结构体。 可以用字段投影方式来给乘积类型赋值：

def location : Float × Float where fst := 22.807 snd := -13.923

4.4.2.4. 结构体继承🔗

结构体可以通过可选的 Lean.Parser.Command.structure : commandextends 子句继承其它结构体。 结果结构体类型将包含所有父结构体的全部字段。 如果父结构体字段有重名，所有同名字段必须同类型。

继承结果结构体有一个 字段解析顺序，决定字段的最终取值。 一般来说，该顺序采用 C3 线性化。 即字段解析顺序是所有父结构体列表的一个全序排列（保留 extends 语句顺序），如果无法形成 C3 线性化，则采用启发式算法排序。 结构体自身在解析顺序中最前。

字段解析顺序用于计算可选字段的默认值。 如未指定字段值，则使用解析顺序中第一个定义了默认的值。 默认值中若引用了其它字段，也采用字段解析顺序；这意味着子结构体如重写了父结构体的默认字段，也可影响父结构体的默认字段的计算结果。 由于子结构体自带最高优先级，因此子结构体中的默认值优先生效于父结构体。

结构体继承其它结构体时，新结构体的构造子会接受父类型的信息作为附加参数。 通常每个父结构体会作为一个参数传递，其值包含父结构体的全部字段。 如果父结构体有重叠字段，则只保留不重叠的那部分，以避免字段重复。

父类型与子类型之间没有子类型关系。 即使结构体 B 继承于 A，期望 A 的函数也不会接受 B 类型。 但系统会自动生成转换函数，将结构体转为各自的父结构体类型。 这些转换函数称为 父投影。 父投影函数定义在子结构体的命名空间中，形式为父类型名加前缀 to。

结构体类型继承与字段重叠

In this example, a Textbook is a Book that is also an AcademicWork:

structure Book where title : String author : String structure AcademicWork where author : String discipline : String structure Textbook extends Book, AcademicWork Textbook.toBook (self : Textbook) : Book#check Textbook.toBook

因为 author 字段同时出现在 Book 与 AcademicWork，所以 Textbook.mk 构造子只需传入一个父实例。 其签名为：

Textbook.mk (toBook : Book) (discipline : String) : Textbook

转换函数为：

Textbook.toBook (self : Textbook) : BookTextbook.toAcademicWork (self : Textbook) : AcademicWork

后一函数会将包含的 Book 的 author 字段与独立的 Discipline 字段组合，等价于：

def toAcademicWork (self : Textbook) : AcademicWork := let .mk book discipline := self let .mk _title author := book .mk author discipline

最终结构体的投影用法上就像字段是所有父结构体字段的并集一样。 Lean 的繁释器会在使用字段时自动生成合适的投影。 同样，基于字段的初始化与结构体更新语法可以隐藏继承实现的细节。 但如果直接使用构造子名称、匿名构造子语法，或者按索引而非字段名称引用字段时，这些细节是可见的。

字段索引与结构体继承
structure Pair (α : Type u) where fst : α snd : α deriving Repr structure Triple (α : Type u) extends Pair α where thd : α deriving Repr def coords : Triple Nat := {fst := 17, snd := 2, thd := 95}

对 coords 的第一字段索引求值时，得到的是 Pair，而不是字段 fst 的值：

{ fst := 17, snd := 2 }#eval coords.1 
{ fst := 17, snd := 2 }

繁释器会自动将 coords.fst 转换为 coords.toPair.fst。

无结构体子类型关系

如下定义偶数、偶质数和具体偶质数：

structure EvenNumber where val : Nat isEven : 2 ∣ val := by decide structure EvenPrime extends EvenNumber where notOne : val ≠ 1 := by decide isPrime : ∀ n, n ≤ val → n ∣ val → n = 1 ∨ n = val def two : EvenPrime where val := 2 isPrime := ⊢ ∀ (n : Nat), n ≤ 2 → n ∣ 2 → n = 1 ∨ n = 2 n✝:Nata✝¹:n✝ ≤ 2a✝:n✝ ∣ 2⊢ n✝ = 1 ∨ n✝ = 2 repeat' (a✝:0 ∣ 2⊢ 0 = 1 ∨ 0 = 2) all_goals All goals completed! 🐙 def printEven (num : EvenNumber) : IO Unit := IO.print num.val

直接将 printEven 应用于 two 会产生类型错误：

printEven sorry : IO Unit#check printEven Application type mismatch: In the application printEven two the argument two has type EvenPrime : Type but is expected to have type EvenNumber : Typetwo 
Application type mismatch: In the application
  printEven two
the argument
  two
has type
  EvenPrime : Type
but is expected to have type
  EvenNumber : Type

因为 EvenPrime 类型的值并非 EvenNumber 类型值。

Lean.Parser.Command.print : command#print 命令能展示所有结构体类型的重要信息，包括 父投影、所有字段（含默认值）、构造子及 字段解析顺序。 对于包含复杂继承菱形的层次结构而言，这些信息非常有用。

#print 与结构体类型

以下是关于自行车的结构体抽象，涵盖电动/非电动、大型/普通家庭自行车。 最后一种结构体 ElectricFamilyBike 形成了继承图中的“菱形”，因为 FamilyBike 和 ElectricBike 都继承自 Bicycle。

structure Vehicle where wheels : Nat structure Bicycle extends Vehicle where wheels := 2 structure ElectricVehicle extends Vehicle where batteries : Nat := 1 structure FamilyBike extends Bicycle where wheels := 3 structure ElectricBike extends Bicycle, ElectricVehicle structure ElectricFamilyBike extends FamilyBike, ElectricBike where batteries := 2

Lean.Parser.Command.print : command#print 可以显示各结构体类型的重要信息：

structure ElectricBike : Type number of parameters: 0 parents: ElectricBike.toBicycle : Bicycle ElectricBike.toElectricVehicle : ElectricVehicle fields: Vehicle.wheels : Nat := 2 ElectricVehicle.batteries : Nat := 1 constructor: ElectricBike.mk (toBicycle : Bicycle) (batteries : Nat) : ElectricBike field notation resolution order: ElectricBike, Bicycle, ElectricVehicle, Vehicle#print ElectricBike 
structure ElectricBike : Type
number of parameters: 0
parents:
  ElectricBike.toBicycle : Bicycle
  ElectricBike.toElectricVehicle : ElectricVehicle
fields:
  Vehicle.wheels : Nat :=
    2
  ElectricVehicle.batteries : Nat :=
    1
constructor:
  ElectricBike.mk (toBicycle : Bicycle) (batteries : Nat) : ElectricBike
field notation resolution order:
  ElectricBike, Bicycle, ElectricVehicle, Vehicle

默认情况下，ElectricFamilyBike 有三轮，因为在解析顺序中 FamilyBike 优先于

structure ElectricFamilyBike : Type number of parameters: 0 parents: ElectricFamilyBike.toFamilyBike : FamilyBike ElectricFamilyBike.toElectricBike : ElectricBike fields: Vehicle.wheels : Nat := 3 ElectricVehicle.batteries : Nat := 2 constructor: ElectricFamilyBike.mk (toFamilyBike : FamilyBike) (batteries : Nat) : ElectricFamilyBike field notation resolution order: ElectricFamilyBike, FamilyBike, ElectricBike, Bicycle, ElectricVehicle, Vehicle#print ElectricFamilyBike 
structure ElectricFamilyBike : Type
number of parameters: 0
parents:
  ElectricFamilyBike.toFamilyBike : FamilyBike
  ElectricFamilyBike.toElectricBike : ElectricBike
fields:
  Vehicle.wheels : Nat :=
    3
  ElectricVehicle.batteries : Nat :=
    2
constructor:
  ElectricFamilyBike.mk (toFamilyBike : FamilyBike) (batteries : Nat) : ElectricFamilyBike
field notation resolution order:
  ElectricFamilyBike, FamilyBike, ElectricBike, Bicycle, ElectricVehicle, Vehicle

4.4.3. 逻辑模型🔗

4.4.3.1. 递归子🔗

每一个归纳类型都拥有一个递归子。 递归子的定义完全由类型构造子和数据构造子的类型签名所决定。 递归子的类型是函数类型，但它们是原语级别的，不能用 fun 来定义。

4.4.3.1.1. 递归子类型🔗

递归子接收以下参数：

归纳类型的参数

由于参数是一致的，所以它们可以对整个递归子抽象

动机(motive)

动机决定了递归子的应用结果的类型。动机是一个函数，其参数是类型的指标及其具体实例。动机决定的类型所处的具体宇宙由归纳类型的宇宙层级和具体的数据构造子决定——详见子单元 消去部分。

每个构造子的次要前提(minor premise)

对于每个构造子，递归子都需要一个函数来满足动机，针对构造子的任意应用。 每个次要前提都对该构造子的所有参数抽象。 如果构造子的某个参数类型是归纳类型本身，那么该前提还要接收一个类型为 对应动机应用到这个参数值 上的参数——这个参数会接收到递归处理该递归参数的结果。

主要前提，或称 目标

最后，递归子接收一个该类型的实例作为参数，以及所有指标的值。

递归子的结果类型，是动机应用于这些指标值和目标的返回值。

Bool 的递归子

Bool 的递归子 Bool.rec 有如下参数：

  • 动机给定一个 Bool，可计算出所属任何宇宙中的类型。

  • 两个构造子都有对应的分支，在这两种情况下，动机分别对 false 和 true 成立。

  • 目标是某个 Bool。

返回类型是动机应用到目标后的结果。

Bool.rec.{u} {motive : Bool → Sort u} (false : motive false) (true : motive true) (t : Bool) : motive t
List 的递归子

List 的递归子 List.rec 有如下参数：

  • 参数 α 在最前，因为参数以及分支都需要引用它

  • 动机在给定一个 List α 时，计算出所属任何宇宙中的类型。这里宇宙层级 u 和 v 没有联系。

  • 两个构造子的分支：

    • 动机对 List.nil 成立

    • 对于 List.cons，只要对尾部成立，同样也应成立。额外的参数 motive tail 是因为 tail 类型是一次递归出现的 List。

  • 目标是某个 List α。

同样，返回类型是动机应用于目标的结果。

List.rec.{u, v} {α : Type v} {motive : List α → Sort u} (nil : motive []) (cons : (head : α) → (tail : List α) → motive tail → motive (head :: tail)) (t : List α) : motive t
带参数和指标的递归子

已知 EvenOddList 的定义如下：

inductive EvenOddList (α : Type u) : Bool → Type u where | nil : EvenOddList α true | cons : α → EvenOddList α isEven → EvenOddList α (not isEven)

EvenOddList.rec 的递归子和 List 类似。 不同之处在于多了一个索引：

  • 动机现在对任意的索引抽象。

  • nil 的分支将动机应用在该构造子的索引值 true 上。

  • cons 分支对其递归出现时使用的索引值抽象，并用指标取反的结果实例化动机。

  • 目标同样对任意索引抽象。

EvenOddList.rec.{u, v} {α : Type v} {motive : (isEven : Bool) → EvenOddList α isEven → Sort u} (nil : motive true EvenOddList.nil) (cons : {isEven : Bool} → (head : α) → (tail : EvenOddList α isEven) → motive isEven tail → motive (!isEven) (EvenOddList.cons head tail)) : {isEven : Bool} → (t : EvenOddList α isEven) → motive isEven t

当动机是一个返回 Prop 的谓词时，递归子就表现为归纳法。 非递归构造子的分支是归纳的基本样例，而递归构造子所额外提供的参数就是归纳假设。

4.4.3.1.1.1. 子单元消去🔗

Lean 中的证明是计算无关的。 换句话说，在给定了某个命题的证明之后，程序应该无法检测到到底是哪一个证明被接受了。 这种思想体现在归纳定义的命题或谓词的递归子的类型中。 对于这些类型，如果定理存在多种可能的证明方式，那么 motive 只能返回另一个 Prop。 如果类型的结构保证了至多只存在一个证明，那么 motive 可以返回任意宇宙中的类型。 拥有至多一个元素的命题被称为 子单元。 Lean 并不会强制用户去证明某命题只有唯一的证明，而是采用了一种保守的语法近似方法来检测一个命题是否为子单元。 满足以下两个条件的命题会被视为子单元（subsingleton）：

  • 至多只有一个构造子。

  • 每个构造子的参数类型要么是 Prop，要么是参数或者索引。

True 是子单元

True 是子单元，因为它仅有一个无参数的构造子。 它的递归子类型如下：

True.rec.{u} {motive : True → Sort u} (intro : motive True.intro) (t : True) : motive t
False 是子单元

False 是子单元，因为它没有构造子。 它的递归子类型如下：

False.rec.{u} (motive : False → Sort u) (t : False) : motive t

注意动机是一个显式参数。 因为它在后续参数类型中没有出现，因此不能自动推断它。

And 是子单元

And 是子单元，因为它仅有一个构造子，并且这个构造子的两个参数类型都是命题。 它的递归子类型如下：

And.rec.{u} {a b : Prop} {motive : a ∧ b → Sort u} (intro : (left : a) → (right : b) → motive (And.intro left right)) (t : a ∧ b) : motive t
Or 不是子单元

Or 不是子单元，因为它有多个构造子。 它的递归子类型如下：

Or.rec {a b : Prop} {motive : a ∨ b → Prop} (inl : ∀ (h : a), motive (.inl h)) (inr : ∀ (h : b), motive (.inr h)) (t : a ∨ b) : motive t

动机的类型表明 Or.rec 只能用于产生证明。 对析取命题提供的证明也能用来证明其它命题，但程序无法判别具体是哪个分支为真。

Eq 是子单元

Eq 是子单元，因为它只有一个构造子 Eq.refl。 构造子会用参数值实例化 Eq 的索引，因此所有参数都是参数项：

Eq.refl.{u} {α : Sort u} (x : α) : Eq x x

它的递归子类型如下：

Eq.rec.{u, v} {α : Sort v} {x : α} {motive : (y : α) → x = y → Sort u} (refl : motive x (.refl x)) {y : α} (t : x = y) : motive y t

意味着等式证明可以用来重写非命题类型的类型。

4.4.3.1.2. 规约🔗

归纳类型声明除了为逻辑添加新常量外，还会引入新的规约规则。 这些规则负责处理递归子和数据构造子之间的互动，尤其是以构造子为目标的递归子的简化行为。 这种规约形式称为 ι-规约（iota reduction）。

当递归子的目标是没有递归参数的构造子时，递归子应用会规约为将该构造子的分支作用于其参数的结果。 如果有递归参数，则这些传递给分支的参数是通过将递归子递归应用于递归出现的参数获得。

4.4.3.2. 良构性约束🔗

归纳类型声明需要满足一系列良构性约束。 这些约束确保当逻辑扩展进入新的归纳类型规则时，Lean 的逻辑系统依然保持一致。 这些约束是保守的：一些不会破坏一致性的归纳类型会被这些约束拒绝。

4.4.3.2.1. 宇宙层级🔗

归纳类型的类型构造子必须处于某个宇宙中，或是返回类型为宇宙的函数类型。 每个数据构造子的类型必须是返回饱和应用归纳类型的函数类型。 如果归纳类型的宇宙是 Prop，则对宇宙没有进一步的限制，因为 Prop 是非直谓的。 如果宇宙不是 Prop，那么以下要求必须成立，对每一个数据构造子的参数都适用：

  • 若构造子的参数是归纳类型的参数（即参数 vs 索引），则该参数类型不能超过类型构造子的宇宙层级。

  • 其它所有构造子参数的类型都必须严格小于类型构造子的宇宙层级。

宇宙、构造子和参数

Either 处于其两个参数宇宙层级的最大值，因为两个参数都是归纳类型的参数：

inductive Either (α : Type u) (β : Type v) : Type (max u v) where | inl : α → Either α β | inr : β → Either α β

CanRepr 的宇宙层级比构造子参数 α 要更高，因为 α 不是归纳类型的参数：

inductive CanRepr : Type (u + 1) where | mk : (α : Type u) → [Repr α] → CanRepr

无构造子的归纳类型的宇宙可以比参数的宇宙更小：

inductive Spurious (α : Type 5) : Type 0 where

但对 Spurious 若要添加构造子，其宇宙层级也必须做相应改变。

4.4.3.2.2. 严格正性🔗

所有定义中的类型在构造子参数类型中的出现都必须处于严格正性的位置。 如果一个类型不处于函数的参数类型里（无论嵌套了多少层函数类型），也不作为任何表达式（除归纳类型的类型构造子外）的参数，那它就是严格正性的位置。 该限制用来排除不安全的归纳类型定义，虽有可能因此排除掉某些良构类型。

非严格正性的归纳类型

类型 Bad 若能通过编译会导致 Lean 不一致：

(kernel) arg #1 of 'Bad.bad' has a non positive occurrence of the datatypes being declaredinductive Bad where | bad : (Bad → Bad) → Bad 
(kernel) arg #1 of 'Bad.bad' has a non positive occurrence of the datatypes being declared

之所以这样，是因为如果假定 Bad 成立，则可以构造出环状逻辑从而证明 False。 Bad.bad 会被拒绝，是因为构造子的参数类型是 Bad → Bad，也就是 Bad 作为函数参数出现。

以下这个不动点算子类型的定义也会被拒绝，因为 Fix 在 f 的参数中出现：

(kernel) arg #2 of 'Fix.fix' contains a non valid occurrence of the datatypes being declaredinductive Fix (f : Type u → Type u) where | fix : f (Fix f) → Fix f 
(kernel) arg #2 of 'Fix.fix' contains a non valid occurrence of the datatypes being declared

Fix.fix 会被拒绝，因为 f 并不是某个归纳类型的类型构造子，而 Fix 在这里作为它的参数出现。 实际上，用 Fix 完全可以构造出等价于 Bad 的类型：

def Bad : Type := Fix fun t => t → t

4.4.3.2.3. Prop vs Type🔗

Lean 会拒绝那些实际上无法多态使用的宇宙多态类型。 例如，如果对宇宙参数的部分实例化会导致类型变成 Prop，而该类型又不是子单元，则其递归子只允许针对命题（即动机只能返回 Prop）。 这些类型实际上只适合充当 Prop 本身，所以宇宙多态很可能本就是错误。 由于这种类型几乎无实际意义，Lean 的归纳类型繁释器并未设计为支持它们。

如果这种宇宙多态归纳类型本身是子单元，则这样的定义还是有意义的。 Lean 的标准库定义了 PUnit 和 PEmpty。 若要定义既可属于 Prop 也可属于 Type 的子单元类型，可将选项 bootstrap.inductiveCheckResultingUniverse 设为 false。

🔗option
bootstrap.inductiveCheckResultingUniverse

默认值: true

默认情况下，如果归纳类型/结构体命令生成的宇宙不是零（universe level 0），即使对某些宇宙参数来说有可能是零，也会报告错误。 原因：除非这个类型是子单元（subsingleton），否则这几乎不是用户想要的，因为它只能消去到 Prop（命题）。 在 Init 前导库包中，我们定义了子单元，并通过此选项关闭该检查。 在将来改进验证器之后，此选项可能会被删除。

过度使用宇宙多态的 Bool

定义一个可以处于任意宇宙的 Bool 是不被允许的：

inductive PBool : invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values: Sort u Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'.Sort u where | true | false 
invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values:
  Sort u
Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'.

4.4.3.3. 用于终止性检查的构造🔗

除了 Lean 核心类型理论为归纳类型规定的类型构造子、数据构造子和递归子外，Lean 还自动生成许多实用的辅助构造。 首先，方程编译器（用于将带模式匹配的递归函数翻译为递归子应用）会用到这些额外构造：

  • recOn 是递归子的一个变体，其目标参数排在每个构造子的分支参数之前。

  • casesOn 也是一个变体，其目标参数也在分支之前，且递归参数不会产生归纳假设。它表达的是分情况分析而非原始递归。

  • below 生成一个类型，表达针对某动机，目标所有子树的所有归纳类型元素都满足该动机。它能把归纳/原始递归用的动机变成强递归/强归纳的动机。

  • brecOn 是使用 below 以可以访问所有子树（而不仅是直接递归参数）的递归子变体，表达强归纳。

  • noConfusion 是一个通用语句，可据此推出构造子的单射性和互斥性。

  • noConfusionType 是为 noConfusion 设计的动机，用以描述两个构造子相等时的推论。对不同构造子而言这是 False；相同构造子则为各自参数的等式。

对于良构递归，通常还需要一个通用意义上的“大小”概念。 这正是 SizeOf 类型类所提供的。

🔗type class
SizeOf.{u} (α : Sort u) : Sort (max 1 u)
SizeOf.{u} (α : Sort u) : Sort (max 1 u)

SizeOf 是每一个归纳类型都会自动派生的类型类， 它为该类型提供了一个到 Nat 的 “大小” 函数。 默认实例会为每个构造子定义其 “大小” 等于 1 加上该构造子所有字段的“大小”之和。

这个机制通常用于良构（well-founded）证明，因为构造子的每个字段的“大小”都比整体构造子本身小， 在许多情况下这就足以证明递归函数只会作用于更小的值。 如果默认的证明策略失败，通常建议在函数定义时通过 termination_by 参数自定义一个大小度量。

Instance Constructor

SizeOf.mk.{u}

Methods

sizeOf : α → Nat

一个元素的“大小”，是一个自然数，在每个归纳类型的字段上会递减。

4.4.4. 运行时表示🔗

归纳类型的运行时表示取决于构造子的数量、每个构造子参数的数量，以及参数是否 相关。

4.4.4.1. 特例🔗

并非所有归纳类型都采用这里描述的表示——部分归纳类型由 Lean 编译器特别支持：

  • 固定宽度整数类型 UInt8、UInt64、Int8、Int64 与 USize 的表示，取决于是为 32 位还是 64 位架构编译。 比指针类型宽度小的固定宽度整数，采用设置指针最低位为 1 的无箱（unbox）方式存储。 长度等于指针宽度的类型，视具体内容可采用无箱或有箱方式：如果实际数值可以用指针位数减一的位表示，则用最低位为 1 区分为 unbox；否则，将其作为指针指向堆上的固定大小 Lean 对象。 在 C FFI 中，这些值会被转为相应的 C 类型 uint8_t、uint64_t、size_t。固定宽度有符号整数类型在 FFI 中也表示为无符号整数。

  • Char 用 uint32_t 表示。由于 Char 取值不超过 21 位，所以总是无箱。

  • Float 由指向包含 double 的 Lean 对象的指针表示。

  • 枚举归纳类型，即至少 2 个、且不超过 2^{32} 个构造子，且构造子无参数的类型，用 uint8_t、uint16_t、uint32_t 中能一一编号的最小类型表示。例如，Bool 用 uint8_t 表示，false 为 0，true 为 1。

  • Decidable α 的表示与 Bool 相同。

  • Nat 和 Int 由 lean_object * 表示。运行时的 Nat 或 Int，要么是指向任意精度整数对象的指针，要么（如“指针”的最低位为 1，经 lean_is_scalar 检查）为 unbox 编码的无箱自然数或整数（相应转换用 lean_box/lean_unbox）。

4.4.4.2. 相关性🔗

类型和证明在运行时没有表示形式。 也就是说，若归纳类型处于 Prop，则其值会在编译前被抹除。 同理，所有定理的陈述和类型都会被抹除。 具有运行时表示的类型称为 相关类型，反之则为 无关类型。

类型是无关的

虽然 List.cons 的签名表面有三个参数：

List.cons.{u} {α : Type u} : α → List α → List α

但运行时实际上只有两个参数，因为类型参数是无关的，不参与运行时表示。

证明是无关的

虽然 Fin.mk 的签名表面有三个参数：

Fin.mk {n : Nat} (val : Nat) : val < n → Fin n

但运行时只有两个参数，因为证明会被抹除。

大多数情况下，无关的值在编译后直接消失。但在少数情况下（如它们是多态构造子的参数时），需要某种“形态”时，会以简单的值表示。

4.4.4.3. 平凡包装类型🔗

如果归纳类型只有一个构造子，且该构造子只有一个运行时相关参数，则该归纳类型的运行时表示与其参数类型完全一致。

零负载子类型

结构体 Subtype 用于将某个类型的元素和满足某谓词的证明打包。 其构造子需要四个参数，但其中三个参数是无关的：

Subtype.mk.{u} {α : Sort u} {p : α → Prop} (val : α) (property : p val) : Subtype p

因此，子类型在编译后不带来运行时额外开销，其表示和 val 字段的类型完全一致。

带符号整数

有符号整数类型 Int8、...、Int64、ISize 是只带唯一字段、该字段包装了对应无符号整数类型的结构体。 因此它们的表示就是无符号 C 类型 uint8_t、...、uint64_t、size_t，因为结构体本身是平凡包装，不带额外信息。

4.4.4.4. 其它归纳类型🔗

如果归纳类型不属于上述类别，则其运行时表示由其构造子结构决定。 没有相关参数的构造子，仅以在构造子列表中的索引（无箱无符号机器整数）表示。 有相关参数的构造子表示为一个对象，该对象有头部信息、构造子索引、指向其它对象的指针数组、以及按照类型分组排序的标量字段数组。 头部用来追踪引用计数以及其它记账信息。

递归函数的编译生成过程与大多数编程语言一致，并不是利用归纳类型的递归子来实现。 将递归函数翻译为递归子只是为了给出可靠的终止证据，而非用于实际执行代码。

4.4.4.4.1. FFI🔗

从 C 语言视角看，其他归纳类型统一用 lean_object * 表示。 每个构造子的存储为一个 lean_ctor_object，且 lean_is_ctor 的返回值为“真”。 lean_ctor_object 在头部存储构造子索引，各字段存放在对象中的 m_objs 区段。Lean 假定 sizeof(size_t) == sizeof(void*)——虽然 C 标准不保证，但 Lean 运行时包含断言，如果这一条件不满足会直接报错。

内存中各字段的布局由声明中的类型及声明顺序决定，排序原则如下：

  • 非标量字段按 lean_object * 存储

  • 类型为 USize 的字段

  • 其它标量字段，按大小从大到小排序

每组内部，字段顺序与声明顺序一致。注意：即使是“平凡包装类型”，只要包装体类型不是标量，也算作非标量字段。

  • 需要访问第一类字段时，用 lean_ctor_get(val, i) 获取第 i 个非标量字段；

  • 访问 USize 字段时，用 lean_ctor_get_usize(val, n+i)，其中 n 是前面所有非标量字段的数目；第 i 个 USize 字段索引为 n+i；

  • 访问其它标量字段，用 lean_ctor_get_uintN(val, off) 或 lean_ctor_get_usize(val, off)，其中 off 是该字段在结构体中的字节偏移，从 n*sizeof(void*)（n 为前两类字段总数）处算起。

For example, a structure such as

structure S where ptr_1 : Array Nat usize_1 : USize sc64_1 : UInt64 -- wrappers don't count as scalars: ptr_2 : { x : UInt64 // x > 0 } sc64_2 : Float -- `Float` is 64 bit sc8_1 : Bool sc16_1 : UInt16 sc8_2 : UInt8 sc64_3 : UInt64 usize_2 : USize -- trivial wrapper around `UInt32` ptr_3 : Char sc32_1 : UInt32 sc16_2 : UInt16

排序后，内存布局如下：

  • S.ptr_1 - lean_ctor_get(val, 0)

  • S.ptr_2 - lean_ctor_get(val, 1)

  • S.ptr_3 - lean_ctor_get(val, 2)

  • S.usize_1 - lean_ctor_get_usize(val, 3)

  • S.usize_2 - lean_ctor_get_usize(val, 4)

  • S.sc64_1 - lean_ctor_get_uint64(val, sizeof(void*)*5)

  • S.sc64_2 - lean_ctor_get_float(val, sizeof(void*)*5 + 8)

  • S.sc64_3 - lean_ctor_get_uint64(val, sizeof(void*)*5 + 16)

  • S.sc32_1 - lean_ctor_get_uint32(val, sizeof(void*)*5 + 24)

  • S.sc16_1 - lean_ctor_get_uint16(val, sizeof(void*)*5 + 28)

  • S.sc16_2 - lean_ctor_get_uint16(val, sizeof(void*)*5 + 30)

  • S.sc8_1 - lean_ctor_get_uint8(val, sizeof(void*)*5 + 32)

  • S.sc8_2 - lean_ctor_get_uint8(val, sizeof(void*)*5 + 33)

4.4.5. 互递归归纳类型🔗

归纳类型之间可以互相递归。 互递归的归纳类型需在 mutual ... end 代码块中统一声明。

互递归归纳类型

在前面的例子中，类型 EvenOddList 用 Boolean 索引来区分列表是偶数还是奇数长度。 这个区分也可以用两个互递归类型 EvenList 和 OddList 表达：

mutual inductive EvenList (α : Type u) : Type u where | nil : EvenList α | cons : α → OddList α → EvenList α inductive OddList (α : Type u) : Type u where | cons : α → EvenList α → OddList α end example : EvenList String := .cons "x" (.cons "y" .nil) example : OddList String := .cons "x" (.cons "y" (.cons "z" .nil)) example : OddList String := .cons "x" (.cons "y" .nilinvalid dotted identifier notation, unknown identifier `OddList.nil` from expected type OddList String) 
invalid dotted identifier notation, unknown identifier `OddList.nil` from expected type
  OddList String

4.4.5.1. 要求🔗

mutual 块中的归纳类型视为一个整体；它们必须一起满足对非互递归归纳类型良构性条件的泛化要求。 即便这些类型单独也可以用非互递归方式定义，只要它们放在 mutual 块内，也要集体满足这些要求。

4.4.5.1.1. 互相关系🔗

每个类型构造子的签名必须可以脱离同组其它类型独立完成繁释。 换句话说，mutual 组内的归纳类型不得作为其它归纳类型的参数。 而各个类型的构造子可以在参数类型中引用本组的其它类型构造子，但需遵守与普通递归情形类似的（严格）限制。

类型构造子之间不能互相引用

下述归纳类型 Lean 不接受：

mutual inductive FreshList (α : Type) (r : α → α → Prop) : Type where | nil : FreshList α r | cons (x : α) (xs : FreshList α r) (fresh : Fresh r x xs) invalid mutually inductive types, binder annotation mismatch at parameter 'α'inductive Fresh (r : α → unknown identifier 'FreshList'FreshList α → Prop) : α → unknown identifier 'FreshList'FreshList α r → Prop where | nil : Fresh r x .nil | cons : r x y → (f : Fresh r x ys) → Fresh r x (.cons y ys f) end

类型构造子不能出现在同组另一个归纳类型的签名中，所以 FreshList 在 Fresh 的类型构造子中不可见：

unknown identifier 'FreshList'

4.4.5.1.2. 参数必须匹配🔗

同一个 mutual 组中的所有归纳类型，参数 必须类型完全一致。 索引可以不同。

参数类型不一致

即便 Many 和 OneOf 之间不存在互递归，只要在同一个 mutual 块声明，也必须参数类型完全一样。两者参数数目一致，但 Many 的参数可能不在 Optional 的宇宙层级：

mutual inductive Both (α : Type u) (β : Type v) where | mk : α → β → Both α β invalid inductive type, number of parameters mismatch in mutually inductive datatypesinductive Optional (α : Type u) where | none | some : α → Optional α end 
invalid inductive type, number of parameters mismatch in mutually inductive datatypes
参数类型不一致

即便 Many 和 OneOf 之间不存在互递归，只要在同一个 mutual 块声明，也必须参数类型完全一样。 两者参数数目一致，但 Many 的参数可能不在 Optional 的宇宙层级：

mutual inductive Many (α : Type) : Type u where | nil : Many α | cons : α → Many α → Many α invalid mutually inductive types, parameter 'α' has type Type u : Type (u + 1) but is expected to have type Type : Type 1inductive Optional (α : Type u) where | none | some : α → Optional α end 
invalid mutually inductive types, parameter 'α' has type
  Type u : Type (u + 1)
but is expected to have type
  Type : Type 1

4.4.5.1.3. 宇宙层级🔗

互递归组中每个归纳类型的宇宙层级，同样需满足非互递归归纳类型的宇宙要求。 另外，所有 mutual 组的类型必须位于同一宇宙，这意味着它们的构造子的参数也要受宇宙层级统一的限制。

宇宙层级不一致

这些互递归类型可以表示列表的行程编码（run-length encoding）：

mutual inductive RLE : List α → Type where | nil : RLE [] | run (x : α) (n : Nat) : n ≠ 0 → PrefixRunOf n x xs ys → RLE ys → RLE xs inductive PrefixRunOf : Nat → α → List α → List α → Type where | zero (noMore : ¬∃zs, xs = x :: zs := by simp) : PrefixRunOf 0 x xs xs | succ : PrefixRunOf n x xs ys → PrefixRunOf (n + 1) x (x :: xs) ys end example : RLE [1, 1, 2, 2, 3, 1, 1, 1] := .run 1 2 (⊢ 2 ≠ 0 All goals completed! 🐙) (.succ (.succ .zero)) <| .run 2 2 (⊢ 2 ≠ 0 All goals completed! 🐙) (.succ (.succ .zero)) <| .run 3 1 (⊢ 1 ≠ 0 All goals completed! 🐙) (.succ .zero) <| .run 1 3 (⊢ 3 ≠ 0 All goals completed! 🐙) (.succ (.succ (.succ (.zero)))) <| .nil

若将 PrefixRunOf 声明为 Prop 会更有意义，但类型因此不在同一宇宙，导致无法通过类型检查：

mutual inductive RLE : List α → Type where | nil : RLE [] | run (x : α) (n : Nat) : n ≠ 0 → PrefixRunOf n x xs ys → RLE ys → RLE xs invalid mutually inductive types, resulting universe mismatch, given Prop expected type Typeinductive PrefixRunOf : Nat → α → List α → List α → Prop where | zero (noMore : ¬∃zs, xs = x :: zs := by simp) : PrefixRunOf 0 x xs xs | succ : PrefixRunOf n x xs ys → PrefixRunOf (n + 1) x (x :: xs) ys end 
invalid mutually inductive types, resulting universe mismatch, given
  Prop
expected type
  Type

这里也可以将性质单独定义，再通过子类型表达：

def RunLengths α := List (α × Nat) def NoRepeats : RunLengths α → Prop | [] => True | [_] => True | (x, _) :: ((y, n) :: xs) => x ≠ y ∧ NoRepeats ((y, n) :: xs) def RunsMatch : RunLengths α → List α → Prop | [], [] => True | (x, n) :: xs, ys => ys.take n = List.replicate n x ∧ RunsMatch xs (ys.drop n) | _, _ => False def NonZero : RunLengths α → Prop | [] => True | (_, n) :: xs => n ≠ 0 ∧ NonZero xs structure RLE (xs : List α) where rle : RunLengths α noRepeats : NoRepeats rle runsMatch : RunsMatch rle xs nonZero : NonZero rle example : RLE [1, 1, 2, 2, 3, 1, 1, 1] where rle := [(1, 2), (2, 2), (3, 1), (1, 3)] noRepeats := ⊢ NoRepeats [(1, 2), (2, 2), (3, 1), (1, 3)] All goals completed! 🐙 runsMatch := ⊢ RunsMatch [(1, 2), (2, 2), (3, 1), (1, 3)] [1, 1, 2, 2, 3, 1, 1, 1] All goals completed! 🐙 nonZero := ⊢ NonZero [(1, 2), (2, 2), (3, 1), (1, 3)] All goals completed! 🐙

4.4.5.1.4. 正性条件(Positivity)🔗

互递归组中各归纳类型只能“严格正”地出现在所有构造子参数的类型表达式中。 即，对于所有类型的所有构造子的每个参数类型，互递归组内的类型构造子不能出现在任何函数箭头左边，也不能出现在参数位置，除非它正好是某个归纳类型类型构造子的参数。

互递归条件下的严格正性

如下 mutual 组中，Tm 在 Binding.scope 的参数类型里出现了负位置：

mutual (kernel) arg #1 of 'Binding.scope' has a non positive occurrence of the datatypes being declaredinductive Tm where | app : Tm → Tm → Tm | lam : Binding → Tm inductive Binding where | scope : (Tm → Tm) → Binding end

由于 Tm 属于同一个互递归组，故只能严格正性出现。实际却出现在负位置：

(kernel) arg #1 of 'Binding.scope' has a non positive occurrence of the datatypes being declared
嵌套位置

LocatedStx 和 Stx 这组互递归类型，递归出现均不在箭头左侧，且作为归纳类型类型构造子的参数，有严格正性：

mutual inductive LocatedStx where | mk (line col : Nat) (val : Stx) inductive Stx where | atom (str : String) | node (kind : String) (args : List LocatedStx) end

4.4.5.2. 递归子🔗

互递归归纳类型和非互递归归纳类型一样，都提供了原语递归子。 这些递归子会考虑到需要处理组内的其他类型，因此每个归纳类型都会有一个目标参数。 由于在 mutual 组中的所有归纳类型都被要求有相同的参数，递归子依然会首先接收这些参数，并将它们抽象到目标参数和递归子的其余部分上。 此外，因为递归子必须处理组内的其他类型，所以它还需要为组内每个类型的每个构造子提供分支。 实际上，类型之间具体的依赖关系在这里没有被考虑；即使由于互递归依赖关系较少，某些目标参数或构造子分支实际上并非必须，生成的递归子依旧会要求这些内容。

偶数与奇数
mutual inductive Even : Nat → Prop where | zero : Even 0 | succ : Odd n → Even (n + 1) inductive Odd : Nat → Prop where | succ : Even n → Odd (n + 1) end Even.rec {motive_1 : (a : Nat) → Even a → Prop} {motive_2 : (a : Nat) → Odd a → Prop} (zero : motive_1 0 Even.zero) (succ : {n : Nat} → (a : Odd n) → motive_2 n a → motive_1 (n + 1) (Even.succ a)) : (∀ {n : Nat} (a : Even n), motive_1 n a → motive_2 (n + 1) (Odd.succ a)) → ∀ {a : Nat} (t : Even a), motive_1 a tOdd.rec {motive_1 : (a : Nat) → Even a → Prop} {motive_2 : (a : Nat) → Odd a → Prop} (zero : motive_1 0 Even.zero) (succ : ∀ {n : Nat} (a : Odd n), motive_2 n a → motive_1 (n + 1) (Even.succ a)) : (∀ {n : Nat} (a : Even n), motive_1 n a → motive_2 (n + 1) (Odd.succ a)) → ∀ {a : Nat} (t : Odd a), motive_2 a t
表面互递归类型

类型 Two 和 Three 其实互不引用，却作为一个 mutual 组共同声明：

mutual inductive Two (α : Type) where | mk : α → α → Two α inductive Three (α : Type) where | mk : α → α → α → Three α end

Two 的递归子 Two.rec 依然需要 motive 以及 Three 的分支：

Two.rec.{u} {α : Type} {motive_1 : Two α → Sort u} {motive_2 : Three α → Sort u} (mk : (a a_1 : α) → motive_1 (Two.mk a a_1)) : ((a a_1 a_2 : α) → motive_2 (Three.mk a a_1 a_2)) → (t : Two α) → motive_1 t

4.4.5.3. 运行时表示🔗

互递归归纳类型在编译后及运行期的表示，与 非互递归归纳类型 完全一致。 对于互递归归纳类型的限制，是为了保证 Lean 作为一种逻辑的可靠性，不影响实际代码的编译与运行。

4.4.5.4. 嵌套归纳类型🔗

嵌套归纳类型是指这些归纳类型在定义中出现了递归自身类型，并且这些递归出现作为其他归纳类型构造子的参数。 这些递归出现是“嵌套”在其他类型构造子之下的。 只要满足一定条件，嵌套归纳类型就可以转换为互递归归纳类型；这种转换说明它们是可靠的。 在内部，内核会执行这种转换；如果转换成功，那么原有的嵌套归纳类型会被接受。 这样可以避免直接暴露内部转换细节而产生的性能和易用性问题。

嵌套递归出现必须满足以下要求：

  • 它们必须直接嵌套在某个归纳类型的类型构造子之下。对于通过规约才变成嵌套出现的情况是不被接受的。

  • 像构造子的参数这样的本地变量，不允许出现在嵌套递归出现的参数中。

  • 嵌套递归出现必须处于严格正向位置。

Nested Inductive Types

自然数除了用两个构造子定义，也可以通过 Option 来定义：

inductive ONat : Type where | mk (pred : Option ONat)

可以有任意分支数的树，也叫 rose trees，它就是一种嵌套归纳类型：

inductive RTree (α : Type u) : Type u where | empty | node (val : α) (children : List (RTree α))
非法的嵌套归纳类型

这个 rose trees 的定义用了一个 List 的别名，而不是直接使用 List：

abbrev Children := List (kernel) arg #3 of 'RTree.node' contains a non valid occurrence of the datatypes being declaredinductive RTree (α : Type u) : Type u where | empty | node (val : α) (children : Children (RTree α)) 
(kernel) arg #3 of 'RTree.node' contains a non valid occurrence of the datatypes being declared

这种定义方式用于通过一个索引追踪树的深度。构造子 DRTree.node 有一个 自动隐式参数 n，代表所有子树的深度。 然而，像构造子参数这样本地变量，不允许作为嵌套递归出现的参数：

(kernel) invalid nested inductive datatype 'List', nested inductive datatypes parameters cannot contain local variables.inductive DRTree (α : Type u) : Nat → Type u where | empty : DRTree α 0 | node (val : α) (children : List (DRTree α n)) : DRTree α (n + 1) 
(kernel) invalid nested inductive datatype 'List', nested inductive datatypes parameters cannot contain local variables.

下面这个定义在 Option 下嵌入了非严格正向的归纳类型出现：

(kernel) arg #1 of 'WithCheck.check' has a non positive occurrence of the datatypes being declaredinductive WithCheck where | done | check (f : Option WithCheck → Bool) 
(kernel) arg #1 of 'WithCheck.check' has a non positive occurrence of the datatypes being declared

嵌套归纳类型转换为互递归归纳类型的流程如下：

嵌套出现变为新的归纳类型

对嵌套出现的归纳类型会翻译为同一互递归组里的新归纳类型，替换原先的嵌套出现。 这些新归纳类型拥有与外层归纳类型一样的构造子，只是在原参数位置用刚刚翻译后的新类型替代。 原始归纳类型本身定义为重写后类型的别名。如果新类型依然是嵌套归纳类型（比如在 Array 下嵌套，因其构造子要用 List，就需要再次翻译到 List），则重复此流程。

构造嵌套类型之间的转换

在外层归纳类型和新别名，及辅助类型之间，分别自动生成互相转换的函数，这些转换将被证明为互逆关系。

构造子重建

原始类型的每个构造子定义为一个函数，返回翻译后类型的相应构造子，调用时会自动应用必要的转换。

递归子重建

嵌套归纳类型的递归子则是结合翻译后类型的递归子而实现的。 在这一步，嵌套出现的目标会先套上转换函数，而次要前提会以它们作为参数。 构造子之间的互逆性证明是必要的，因为封装后的构造子是单方向转换，但在组合递归结构时需要转换后的结果。

翻译嵌套归纳类型

下面是一个用嵌套归纳类型定义的自然数类型：

inductive ONat where | mk (pred : Option ONat) : ONat ONat.rec.{u} {motive_1 : ONat → Sort u} {motive_2 : Option ONat → Sort u} (mk : (pred : Option ONat) → motive_2 pred → motive_1 (ONat.mk pred)) (none : motive_2 none) (some : (val : ONat) → motive_1 val → motive_2 (some val)) (t : ONat) : motive_1 t#check ONat.rec

内部翻译的第一步，是用辅助归纳类型“内联”嵌套出现的位置。 这里嵌套发生在 Option 之下，所以辅助类型拥有 Option 的构造子，但其类型参数用 ONat' 替代：

mutual inductive ONat' where | mk (pred : OptONat) : ONat' inductive OptONat where | none | some : ONat' → OptONat end

ONat' 就是 ONat 经过编码后的版本：

def ONat := ONat'

下一步是定义转换函数，用于在原始嵌套类型和辅助类型之间相互转换：

def OptONat.ofOption : Option ONat → OptONat | Option.none => OptONat.none | Option.some o => OptONat.some o def OptONat.toOption : OptONat → Option ONat | OptONat.none => Option.none | OptONat.some o => Option.some o

这些相互转换的函数是互逆的：

def OptONat.to_of_eq_id o : OptONat.toOption (ofOption o) = o := o:Option ONat⊢ (ofOption o).toOption = o ⊢ (ofOption Option.none).toOption = Option.noneval✝:ONat⊢ (ofOption (Option.some val✝)).toOption = Option.some val✝ ⊢ (ofOption Option.none).toOption = Option.noneval✝:ONat⊢ (ofOption (Option.some val✝)).toOption = Option.some val✝ All goals completed! 🐙 def OptONat.of_to_eq_id o : OptONat.ofOption (OptONat.toOption o) = o := o:OptONat⊢ ofOption o.toOption = o ⊢ ofOption none.toOption = nonea✝:ONat'⊢ ofOption (some a✝).toOption = some a✝ ⊢ ofOption none.toOption = nonea✝:ONat'⊢ ofOption (some a✝).toOption = some a✝ All goals completed! 🐙

原始的构造子被翻译成对翻译后类型的构造子的调用，同时会对嵌套递归部分做适当类型转换：

def ONat.mk (pred : Option ONat) : ONat := ONat'.mk (.ofOption pred)

最后，原类型的递归子也可以翻译。 翻译后的递归子会通过翻译后类型的递归子来实现。 原本嵌套递归位置会采用相应的转换函数，并且互逆性的证明可以在需要时重写类型：

noncomputable def ONat.rec {motive1 : ONat → Sort u} {motive2 : Option ONat → Sort u} (h1 : (pred : Option ONat) → motive2 pred → motive1 (ONat.mk pred)) (h2 : motive2 none) (h3 : (o : ONat) → motive1 o → motive2 (some o)) : (t : ONat) → motive1 t := @ONat'.rec motive1 (motive2 ∘ OptONat.toOption) (fun pred ih => OptONat.of_to_eq_id pred ▸ h1 pred.toOption ih) h2 h3